Search Results

Documents authored by Itsykson, Dmitry

Document
DOI: 10.4230/LIPIcs.MFCS.2022.59
Automating OBDD proofs is NP-hard

Authors: Dmitry Itsykson and Artur Riazanov

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We prove that the proof system OBDD(∧, weakening) is not automatable unless P = NP. The proof is based upon the celebrated result of [Albert Atserias and Moritz Müller, 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with multi-output indexing gadget from resolution block-width to dag-like multiparty number-in-hand communication protocol size with o(n) parties, where n is the number of variables in the non-lifted formula. A similar lifting theorem for protocols with n+1 participants was proved by [Göös et al., 2020] to establish the hardness of automatability result for Cutting Planes.
Cite as

Dmitry Itsykson and Artur Riazanov. Automating OBDD proofs is NP-hard. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 59:1-59:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.MFCS.2022.59,
  author =	{Itsykson, Dmitry and Riazanov, Artur},
  title =	{{Automating OBDD proofs is NP-hard}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{59:1--59:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.59},
  URN =		{urn:nbn:de:0030-drops-168575},
  doi =		{10.4230/LIPIcs.MFCS.2022.59},
  annote =	{Keywords: proof complexity, OBDD, automatability, lifting, dag-like communication}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.6
Tight Bounds for Tseitin Formulas

Authors: Dmitry Itsykson, Artur Riazanov, and Petr Smirnov

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
We show that for any connected graph G the size of any regular resolution or OBDD(∧, reordering) refutation of a Tseitin formula based on G is at least 2^Ω(tw(G)), where tw(G) is the treewidth of G. These lower bounds improve upon the previously known bounds and, moreover, they are tight. For both of the proof systems, there are constructive upper bounds that almost match the obtained lower bounds, hence the class of Tseitin formulas is almost automatable for regular resolution and for OBDD(∧, reordering).
Cite as

Dmitry Itsykson, Artur Riazanov, and Petr Smirnov. Tight Bounds for Tseitin Formulas. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.SAT.2022.6,
  author =	{Itsykson, Dmitry and Riazanov, Artur and Smirnov, Petr},
  title =	{{Tight Bounds for Tseitin Formulas}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.6},
  URN =		{urn:nbn:de:0030-drops-166805},
  doi =		{10.4230/LIPIcs.SAT.2022.6},
  annote =	{Keywords: Proof complexity, Tseitin formulas, treewidth, resolution, OBDD-based proof systems}
}
Document
DOI: 10.4230/LIPIcs.CCC.2021.3
Proof Complexity of Natural Formulas via Communication Arguments

Authors: Dmitry Itsykson and Artur Riazanov

Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)

Abstract
A canonical communication problem Search(φ) is defined for every unsatisfiable CNF φ: an assignment to the variables of φ is partitioned among the communicating parties, they are to find a clause of φ falsified by this assignment. Lower bounds on the randomized k-party communication complexity of Search(φ) in the number-on-forehead (NOF) model imply tree-size lower bounds, rank lower bounds, and size-space tradeoffs for the formula φ in the semantic proof system T^{cc}(k,c) that operates with proof lines that can be computed by k-party randomized communication protocol using at most c bits of communication [Göös and Pitassi, 2014]. All known lower bounds on Search(φ) (e.g. [Beame et al., 2007; Göös and Pitassi, 2014; Russell Impagliazzo et al., 1994]) are realized on ad-hoc formulas φ (i.e. they were introduced specifically for these lower bounds). We introduce a new communication complexity approach that allows establishing proof complexity lower bounds for natural formulas. First, we demonstrate our approach for two-party communication and apply it to the proof system Res(⊕) that operates with disjunctions of linear equalities over 𝔽₂ [Dmitry Itsykson and Dmitry Sokolov, 2014]. Let a formula PM_G encode that a graph G has a perfect matching. If G has an odd number of vertices, then PM_G has a tree-like Res(⊕)-refutation of a polynomial-size [Dmitry Itsykson and Dmitry Sokolov, 2014]. It was unknown whether this is the case for graphs with an even number of vertices. Using our approach we resolve this question and show a lower bound 2^{Ω(n)} on size of tree-like Res(⊕)-refutations of PM_{K_{n+2,n}}. Then we apply our approach for k-party communication complexity in the NOF model and obtain a Ω(1/k 2^{n/2k - 3k/2}) lower bound on the randomized k-party communication complexity of Search(BPHP^{M}_{2ⁿ}) w.r.t. to some natural partition of the variables, where BPHP^{M}_{2ⁿ} is the bit pigeonhole principle and M = 2ⁿ+2^{n(1-1/k)}. In particular, our result implies that the bit pigeonhole requires exponential tree-like Th(k) proofs, where Th(k) is the semantic proof system operating with polynomial inequalities of degree at most k and k = 𝒪(log^{1-ε} n) for some ε > 0. We also show that BPHP^{2ⁿ+1}_{2ⁿ} superpolynomially separates tree-like Th(log^{1-ε} m) from tree-like Th(log m), where m is the number of variables in the refuted formula.
Cite as

Dmitry Itsykson and Artur Riazanov. Proof Complexity of Natural Formulas via Communication Arguments. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 3:1-3:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.CCC.2021.3,
  author =	{Itsykson, Dmitry and Riazanov, Artur},
  title =	{{Proof Complexity of Natural Formulas via Communication Arguments}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{3:1--3:34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-193-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{200},
  editor =	{Kabanets, Valentine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.3},
  URN =		{urn:nbn:de:0030-drops-142773},
  doi =		{10.4230/LIPIcs.CCC.2021.3},
  annote =	{Keywords: bit pigeonhole principle, disjointness, multiparty communication complexity, perfect matching, proof complexity, randomized communication complexity, Resolution over linear equations, tree-like proofs}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.49
Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs

Authors: Nicola Galesi, Dmitry Itsykson, Artur Riazanov, and Anastasia Sofronova

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
We prove that there is a constant K such that Tseitin formulas for an undirected graph G requires proofs of size 2^{tw(G)^{Omega(1/d)}} in depth-d Frege systems for d<(K log n)/(log log n), where tw(G) is the treewidth of G. This extends Håstad recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent. Namely, we show that if a Tseitin formula for a graph G has size s, then for all large enough d, it has a depth-d Frege proof of size 2^{tw(G)^{O(1/d)}} poly(s). Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.
Cite as

Nicola Galesi, Dmitry Itsykson, Artur Riazanov, and Anastasia Sofronova. Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{galesi_et_al:LIPIcs.MFCS.2019.49,
  author =	{Galesi, Nicola and Itsykson, Dmitry and Riazanov, Artur and Sofronova, Anastasia},
  title =	{{Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{49:1--49:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.49},
  URN =		{urn:nbn:de:0030-drops-109932},
  doi =		{10.4230/LIPIcs.MFCS.2019.49},
  annote =	{Keywords: Tseitin formula, treewidth, AC0-Frege}
}
Document
DOI: 10.4230/LIPIcs.CCC.2018.16
Reordering Rule Makes OBDD Proof Systems Stronger

Authors: Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov

Published in: LIPIcs, Volume 102, 33rd Computational Complexity Conference (CCC 2018)

Abstract
Atserias, Kolaitis, and Vardi showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD(^, weakening), simulates CP^* (Cutting Planes with unary coefficients). We show that OBDD(^, weakening) can give exponentially shorter proofs than dag-like cutting planes. This is proved by showing that the Clique-Coloring tautologies have polynomial size proofs in the OBDD(^, weakening) system. The reordering rule allows changing the variable order for OBDDs. We show that OBDD(^, weakening, reordering) is strictly stronger than OBDD(^, weakening). This is proved using the Clique-Coloring tautologies, and by transforming tautologies using coded permutations and orification. We also give CNF formulas which have polynomial size OBDD(^) proofs but require superpolynomial (actually, quasipolynomial size) resolution proofs, and thus we partially resolve an open question proposed by Groote and Zantema. Applying dag-like and tree-like lifting techniques to the mentioned results, we completely analyze which of the systems among CP^*, OBDD(^), OBDD(^, reordering), OBDD(^, weakening) and OBDD(^, weakening, reordering) polynomially simulate each other. For dag-like proof systems, some of our separations are quasipolynomial and some are exponential; for tree-like systems, all of our separations are exponential.
Cite as

Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering Rule Makes OBDD Proof Systems Stronger. In 33rd Computational Complexity Conference (CCC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 102, pp. 16:1-16:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{buss_et_al:LIPIcs.CCC.2018.16,
  author =	{Buss, Sam and Itsykson, Dmitry and Knop, Alexander and Sokolov, Dmitry},
  title =	{{Reordering Rule Makes OBDD Proof Systems Stronger}},
  booktitle =	{33rd Computational Complexity Conference (CCC 2018)},
  pages =	{16:1--16:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-069-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{102},
  editor =	{Servedio, Rocco A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2018.16},
  URN =		{urn:nbn:de:0030-drops-88720},
  doi =		{10.4230/LIPIcs.CCC.2018.16},
  annote =	{Keywords: Proof complexity, OBDD, Tseitin formulas, the Clique-Coloring principle, lifting theorems}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.26
Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs

Authors: Ludmila Glinskih and Dmitry Itsykson

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We consider satisfiable Tseitin formulas TS_{G,c} based on d-regular expanders G with the absolute value of the second largest eigenvalue less than d/3. We prove that any nondeterministic read-once branching program (1-NBP) representing TS_{G,c} has size 2^{\Omega(n)}, where n is the number of vertices in G. It extends the recent result by Itsykson at el. [STACS 2017] from OBDD to 1-NBP. On the other hand it is easy to see that TS_{G,c} can be represented as a read-2 branching program (2-BP) of size O(n), as the negation of a nondeterministic read-once branching program (1-coNBP) of size O(n) and as a CNF formula of size O(n). Thus TS_{G,c} gives the best possible separations (up to a constant in the exponent) between 1-NBP and 2-BP, 1-NBP and 1-coNBP and between 1-NBP and CNF.
Cite as

Ludmila Glinskih and Dmitry Itsykson. Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 26:1-26:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{glinskih_et_al:LIPIcs.MFCS.2017.26,
  author =	{Glinskih, Ludmila and Itsykson, Dmitry},
  title =	{{Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{26:1--26:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.26},
  URN =		{urn:nbn:de:0030-drops-80767},
  doi =		{10.4230/LIPIcs.MFCS.2017.26},
  annote =	{Keywords: Tseitin formula, read-once branching program, expander}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.43
On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables

Authors: Dmitry Itsykson, Alexander Knop, Andrey Romashchenko, and Dmitry Sokolov

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of identically false OBDD from OBDDs representing clauses of the initial formula. All OBDDs in such proofs have the same order of variables. We initiate the study of OBDD based proof systems that additionally contain a rule that allows to change the order in OBDDs. At first we consider a proof system OBDD(and, reordering) that uses the conjunction (join) rule and the rule that allows to change the order. We exponentially separate this proof system from OBDD(and)-proof system that uses only the conjunction rule. We prove two exponential lower bounds on the size of OBDD(and, reordering)-refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for OBDD(and)-proofs and the second one extends the result of Tveretina et al. from OBDD(and) to OBDD(and, reordering). In 2004 Pan and Vardi proposed an approach to the propositional satisfiability problem based on OBDDs and symbolic quantifier elimination (we denote algorithms based on this approach as OBDD(and, exists)-algorithms. We notice that there exists an OBDD(and, exists)-algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time. In contrast, we show that there exist formulas representing systems of linear equations over F_2 that are hard for OBDD(and, exists, reordering)-algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over F_2 that correspond to some checksum matrices of error correcting codes.
Cite as

Dmitry Itsykson, Alexander Knop, Andrey Romashchenko, and Dmitry Sokolov. On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 43:1-43:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.STACS.2017.43,
  author =	{Itsykson, Dmitry and Knop, Alexander and Romashchenko, Andrey and Sokolov, Dmitry},
  title =	{{On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{43:1--43:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.43},
  URN =		{urn:nbn:de:0030-drops-69914},
  doi =		{10.4230/LIPIcs.STACS.2017.43},
  annote =	{Keywords: Proof complexity, OBDD, error-correcting codes, Tseitin formulas, expanders}
}
Document
DOI: 10.4230/LIPIcs.ISAAC.2016.38
Complexity of Distributions and Average-Case Hardness

Authors: Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov

Published in: LIPIcs, Volume 64, 27th International Symposium on Algorithms and Computation (ISAAC 2016)

Abstract
We address the following question in the average-case complexity: does there exists a language L such that for all easy distributions D the distributional problem (L, D) is easy on the average while there exists some more hard distribution D' such that (L, D') is hard on the average? We consider two complexity measures of distributions: the complexity of sampling and the complexity of computing the distribution function. For the complexity of sampling of distribution, we establish a connection between the above question and the hierarchy theorem for sampling distribution recently studied by Thomas Watson. Using this connection we prove that for every 0 < a < b there exist a language L, an ensemble of distributions D samplable in n^{log^b n} steps and a linear-time algorithm A such that for every ensemble of distribution F that samplable in n^{log^a n} steps, A correctly decides L on all inputs from {0, 1}^n except for a set that has infinitely small F-measure, and for every algorithm B there are infinitely many n such that the set of all elements of {0, 1}^n for which B correctly decides L has infinitely small D-measure. In case of complexity of computing the distribution function we prove the following tight result: for every a > 0 there exist a language L, an ensemble of polynomial-time computable distributions D, and a linear-time algorithm A such that for every computable in n^a steps ensemble of distributions F , A correctly decides L on all inputs from {0, 1}^n except for a set that has F-measure at most 2^{-n/2} , and for every algorithm B there are infinitely many n such that the set of all elements of {0, 1}^n for which B correctly decides L has D-measure at most 2^{-n+1}.
Cite as

Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Complexity of Distributions and Average-Case Hardness. In 27th International Symposium on Algorithms and Computation (ISAAC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 64, pp. 38:1-38:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.ISAAC.2016.38,
  author =	{Itsykson, Dmitry and Knop, Alexander and Sokolov, Dmitry},
  title =	{{Complexity of Distributions and Average-Case Hardness}},
  booktitle =	{27th International Symposium on Algorithms and Computation (ISAAC 2016)},
  pages =	{38:1--38:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-026-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{64},
  editor =	{Hong, Seok-Hee},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2016.38},
  URN =		{urn:nbn:de:0030-drops-68083},
  doi =		{10.4230/LIPIcs.ISAAC.2016.38},
  annote =	{Keywords: average-case complexity, hierarchy theorem, sampling distributions, diagonalization}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.51
Computational and Proof Complexity of Partial String Avoidability

Authors: Dmitry Itsykson, Alexander Okhotin, and Vsevolod Oparin

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
The partial string avoidability problem, also known as partial word avoidability, is stated as follows: given a finite set of strings with possible ``holes'' (undefined symbols), determine whether there exists any two-sided infinite string containing no substrings from this set, assuming that a hole matches every symbol. The problem is known to be NP-hard and in PSPACE, and this paper establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form (CNF) satisfiability problem (SAT), with each clause having infinitely many shifted variants. Non-satisfiability of these formulas can be proved using variants of classical propositional proof systems, augmented with derivation rules for shifting constraints (such as clauses, inequalities, polynomials, etc). Two results on their proof complexity are established. First, there is a particular formula that has a short refutation in Resolution with shift, but requires classical proofs of exponential size (Resolution, Cutting Plane, Polynomial Calculus, etc.). At the same time, exponential lower bounds for shifted versions of classical proof systems are established.
Cite as

Dmitry Itsykson, Alexander Okhotin, and Vsevolod Oparin. Computational and Proof Complexity of Partial String Avoidability. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 51:1-51:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.MFCS.2016.51,
  author =	{Itsykson, Dmitry and Okhotin, Alexander and Oparin, Vsevolod},
  title =	{{Computational and Proof Complexity of Partial String Avoidability}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{51:1--51:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.51},
  URN =		{urn:nbn:de:0030-drops-64637},
  doi =		{10.4230/LIPIcs.MFCS.2016.51},
  annote =	{Keywords: partial strings, partial words, avoidability, proof complexity, PSPACE-completeness}
}
Document
DOI: 10.4230/LIPIcs.STACS.2010.2475
On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity

Authors: Edward A. Hirsch and Dmitry Itsykson

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

Abstract
The existence of a ($p$-)optimal propositional proof system is a major open question in (proof) complexity; many people conjecture that such systems do not exist. Kraj\'{\i}\v{c}ek and Pudl\'{a}k \cite{KP} show that this question is equivalent to the existence of an algorithm that is optimal\footnote{Recent papers \cite{Monroe} call such algorithms \emph{$p$-optimal} while traditionally Levin's algorithm was called \emph{optimal}. We follow the older tradition. Also there is some mess in terminology here, thus please see formal definitions in Sect.~\ref{sec:prelim} below.} on all propositional tautologies. Monroe \cite{Monroe} recently gave a conjecture implying that such algorithm does not exist. We show that in the presence of errors such optimal algorithms \emph{do} exist. The concept is motivated by the notion of heuristic algorithms. Namely, we allow the algorithm to claim a small number of false ``theorems'' (according to any polynomial-time samplable distribution on non-tautologies) and err with bounded probability on other inputs. Our result can also be viewed as the existence of an optimal proof system in a class of proof systems obtained by generalizing automatizable proof systems.
Cite as

Edward A. Hirsch and Dmitry Itsykson. On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 453-464, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{hirsch_et_al:LIPIcs.STACS.2010.2475,
  author =	{Hirsch, Edward A. and Itsykson, Dmitry},
  title =	{{On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{453--464},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2475},
  URN =		{urn:nbn:de:0030-drops-24753},
  doi =		{10.4230/LIPIcs.STACS.2010.2475},
  annote =	{Keywords: Propositional proof complexity, optimal algorithm}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact